gnome-shell-extension-prefs: Give Debian-specific advice

We package gnome-extensions-app in the same binary package as
gnome-shell-extension-prefs, so there's never a need to download it from
Flathub.

Forwarded: not-needed, Debian-specific
Signed-off-by: Simon McVittie <smcv@debian.org>
Gbp-Pq: Topic debian
Gbp-Pq: Name gnome-shell-extension-prefs-Give-Debian-specific-advice.patch

diff --git a/src/gnome-shell-extension-prefs b/src/gnome-shell-extension-prefs
index 303b1963c0d22f4d18241f4f196b3e03da22a46a..a59ffed125354da14c4891a9d92d602098a772d6 100755 (executable)
--- a/src/gnome-shell-extension-prefs
+++ b/src/gnome-shell-extension-prefs
@@ -13,10 +13,10 @@ openPrefs() {
 }
 
 cat >&2 <<EOT
-gnome-shell-extension-prefs is deprecated
+The gnome-shell-extension-prefs program is deprecated.
 
-Install https://flathub.org/apps/details/org.gnome.Extensions for extension
-management, or use the gnome-extensions command line tool.
+Run gnome-extensions-app (from the gnome-shell-extension-prefs package)
+for extension management, or use the gnome-extensions command line tool.
 
 Extensions can use the ExtensionUtils.openPrefs() method.
 EOT